COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00003 ENDMK
C⊗;

axiom blah:
	∀w X x.(basic X ⊃ denot(a(X,x,w),X) = x)
	∀w X1 X2 x.(basic X1 ∧ basic X2 ∧ ¬(X1=X2) ⊃ denot(a(X1,x,w),X2)
= denot(w,X2))
;;

axiom arithmetic:
	∀P w N1 N2.(true(w,Know(P,N1)) ∧ true(w,Know(P,N2))
⊃ true(w,Know(P, N1 Plus N2)))
;;